Section: New Results

Constructive mathematics

Participant : Cyril Cohen [Contact] .

In collaboration with Thierry Coquand, Cyril Cohen has come up with a constructive proof of a generalization of the fundamental theorem of Algebra. This work show how to formalize the algebraic closure of an arbitrary real closed field. In particular, it can serve as a basis for the construction of complex algebraic numbers from the real algebraic numbers. This work is described in a submitted paper [28] .